ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-ex(x)   List 

latex

Definitions	x:A. B(x), t  T, , ecl-ex(x), if b t else f fi, x,y. t(x;y), x,y,z,w. t(x;y;z;w), P  Q, x,y,z. t(x;y;z), true, Prop, false, x. t(x), , , x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), Unit, P  Q, P & Q, A, AB, False, x(s),
Lemmas	nat plus wf, ecl ind wf, decl-state wf, ma-valtype wf, bool wf, merge wf, nat wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, s-insert wf, ecl wf, fpf wf, Knd wf, Id wf